$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), $a$:$T$, $L$:($T$ List).
\\[0ex]($\forall$$b$:$T$. ($b$ $\in$ insert(${\it eq}$; $a$; $L$)) $\Leftarrow\!\Rightarrow$ (($b$ = $a$) $\vee$ ($b$ $\in$ $L$)))
\\[0ex]$\wedge$ (no\_repeats($T$; $L$) $\Rightarrow$ no\_repeats($T$; insert(${\it eq}$; $a$; $L$)))